Section: New Results

Compositional verification

BDD-based assume-guarantee reasoning through implicit learning

Participants : Fei He, Bow-Yaw Wang, Lei Zhu.

We present a purely BDD-based assume-guarantee reasoning technique to improve the scalability of symbolic model checking. The new technique adopts a BDD learning algorithm to generate BDD's as contextual assumptions. A new witness analysis algorithm is proposed to exploit the multitude of traces returned by symbolic model checkers. Using the classification tree-based BDD learning algorithm to generate contextual assumptions, we compare assume-guarantee reasoning with monolithic symbolic model checking. The new technique always infers smaller contextual assumptions than contexts in our experiments.

Predicate generation for learning-based loop invariant inference

Participant : Bow-Yaw Wang.

We address the predicate generation problem in the context of loop invariant inference. Motivated by the interpolation-based abstraction refinement technique, we apply the interpolation theorem to synthesize predicates implicitly implied by program texts. Our technique is able to improve the effectiveness and efficiency of the learning-based loop invariant inference algorithm in [21] . Experiments excerpted from Linux, SPEC2000, and Tar source codes are reported.

This is a joint work with Yungbum Jung, Wonchan Lee, and Kwangkuen Yi of Seoul National University, South Korea.

Thread-modular model checking with iterative refinement

Participants : Wenrui Meng, Fei He, Bow-Yaw Wang.

Thread-modular analysis is an incomplete compositional technique for verifying concurrent systems. The heuristic works rather well when there is limited interaction among system components. In this project, we develop a refinement algorithm that makes thread-modular model checking complete. Our algorithm refines abstract reachable states by exposing local information through auxiliary variables. The experiments show that our complete thread-modular model checking can outperform other complete compositional reasoning techniques.